the_es:ES, l:IdLnk, e:E. haslnk(l;e)   

latex

Definitions	x:A. B(x), t  T, haslnk(l;e), p  q, if b then t else f fi , ff, P  Q, tt, , Dec(P), P  Q, A, , Unit, P  Q, P & Q, False,
Lemmas	decidable assert, es-isrcv wf, band wf, eq lnk wf, es-lnk wf, es-E wf, IdLnk wf, event system wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, bfalse wf